FDL - Nuprl Lemma : gcd_p_mul

Nuprl Lemma : gcd_p_mul

a, b, y, n:

. GCD(a;b;y)

GCD(n

a;n

b;n

y)

Definitions P Q, P & Q, Prop, b | a, GCD(a;b;y), x:A. B(x), t T, x:A. B(x), P Q, P Q, T, True

Lemmas true wf, squash wf, divisor of sum, divisor of mul, assoced weakening, multiply functionality wrt assoced, divides functionality wrt assoced, gcd unique, bezout ident, divides mul, gcd p wf, divides wf